(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 12))
(declare-fun v1 () (_ BitVec 5))
(declare-fun v2 () (_ BitVec 7))
(declare-fun v3 () (_ BitVec 1))
(declare-fun v4 () (_ BitVec 13))
(assert (let ((e5(_ bv0 1)))
(let ((e6 ((_ rotate_right 0) v3)))
(let ((e7 ((_ extract 0 0) e5)))
(let ((e8 ((_ sign_extend 11) e6)))
(let ((e9 (ite (bvugt e7 e6) (_ bv1 1) (_ bv0 1))))
(let ((e10 (bvcomp v0 ((_ zero_extend 11) v3))))
(let ((e11 (ite (bvsgt e9 e5) (_ bv1 1) (_ bv0 1))))
(let ((e12 (bvxnor v0 v0)))
(let ((e13 (bvmul v0 ((_ zero_extend 11) e6))))
(let ((e14 ((_ sign_extend 7) e10)))
(let ((e15 (concat v3 e12)))
(let ((e16 (bvcomp ((_ zero_extend 2) v1) v2)))
(let ((e17 ((_ extract 0 0) v3)))
(let ((e18 (bvadd v1 ((_ sign_extend 4) e17))))
(let ((e19 (bvnot e18)))
(let ((e20 (bvnor e7 v3)))
(let ((e21 ((_ rotate_right 6) e8)))
(let ((e22 ((_ repeat 1) v2)))
(let ((e23 (bvsrem ((_ zero_extend 5) v2) e12)))
(let ((e24 ((_ sign_extend 7) e19)))
(let ((e25 (ite (bvult e20 e11) (_ bv1 1) (_ bv0 1))))
(let ((e26 (concat e8 e11)))
(let ((e27 (ite (bvult ((_ zero_extend 2) v1) v2) (_ bv1 1) (_ bv0 1))))
(let ((e28 (bvsub ((_ sign_extend 6) v2) e15)))
(let ((e29 (bvxor e18 ((_ sign_extend 4) e27))))
(let ((e30 (bvmul e29 ((_ sign_extend 4) e11))))
(let ((e31 (bvshl e21 ((_ sign_extend 7) v1))))
(let ((e32 ((_ zero_extend 14) e5)))
(let ((e33 (ite (bvsle e15 ((_ sign_extend 8) e29)) (_ bv1 1) (_ bv0 1))))
(let ((e34 (bvlshr e23 ((_ sign_extend 7) e19))))
(let ((e35 (ite (distinct e33 e11) (_ bv1 1) (_ bv0 1))))
(let ((e36 (bvnot e7)))
(let ((e37 (bvnot e32)))
(let ((e38 ((_ sign_extend 0) e7)))
(let ((e39 (bvsrem ((_ sign_extend 14) e25) e37)))
(let ((e40 (ite (bvslt v4 ((_ sign_extend 1) e24)) (_ bv1 1) (_ bv0 1))))
(let ((e41 (= e11 e17)))
(let ((e42 (bvule e39 ((_ sign_extend 3) v0))))
(let ((e43 (bvsle ((_ zero_extend 11) e25) e23)))
(let ((e44 (bvugt ((_ sign_extend 14) e11) e32)))
(let ((e45 (bvsgt ((_ sign_extend 10) e30) e37)))
(let ((e46 (bvsge e32 ((_ zero_extend 14) e38))))
(let ((e47 (bvule ((_ zero_extend 11) e33) e31)))
(let ((e48 (bvult e12 ((_ sign_extend 11) e5))))
(let ((e49 (bvsle ((_ sign_extend 12) e9) e26)))
(let ((e50 (bvult ((_ sign_extend 12) e25) e26)))
(let ((e51 (bvsgt ((_ sign_extend 11) e11) e12)))
(let ((e52 (bvugt ((_ sign_extend 11) e33) e34)))
(let ((e53 (bvslt ((_ zero_extend 11) e36) e23)))
(let ((e54 (= e35 e17)))
(let ((e55 (bvsle e21 ((_ sign_extend 7) e18))))
(let ((e56 (bvsle e8 e21)))
(let ((e57 (bvule v4 ((_ zero_extend 1) e21))))
(let ((e58 (bvslt ((_ sign_extend 12) e6) e26)))
(let ((e59 (bvsgt v4 ((_ zero_extend 1) e24))))
(let ((e60 (bvsgt ((_ sign_extend 2) e26) e37)))
(let ((e61 (bvugt e12 ((_ zero_extend 11) e7))))
(let ((e62 (bvuge ((_ zero_extend 4) e7) e30)))
(let ((e63 (bvugt ((_ sign_extend 10) e29) e32)))
(let ((e64 (distinct e34 ((_ sign_extend 5) e22))))
(let ((e65 (bvugt e18 ((_ sign_extend 4) v3))))
(let ((e66 (bvugt e15 ((_ zero_extend 12) e40))))
(let ((e67 (bvsle ((_ zero_extend 4) e40) e29)))
(let ((e68 (bvult ((_ zero_extend 6) e25) e22)))
(let ((e69 (bvsge e12 e23)))
(let ((e70 (bvuge v3 e20)))
(let ((e71 (bvsle e40 e40)))
(let ((e72 (bvuge ((_ sign_extend 11) e9) e13)))
(let ((e73 (= e36 e10)))
(let ((e74 (bvule e34 ((_ sign_extend 11) v3))))
(let ((e75 (= e37 ((_ sign_extend 2) v4))))
(let ((e76 (bvule e39 ((_ zero_extend 14) e20))))
(let ((e77 (bvsge e13 ((_ zero_extend 11) e9))))
(let ((e78 (distinct ((_ zero_extend 4) e14) v0)))
(let ((e79 (bvsgt e10 e36)))
(let ((e80 (bvslt ((_ zero_extend 11) e9) e21)))
(let ((e81 (= ((_ zero_extend 3) v1) e14)))
(let ((e82 (bvule ((_ zero_extend 12) e17) e26)))
(let ((e83 (bvsgt e19 e30)))
(let ((e84 (bvsge e32 ((_ sign_extend 14) e20))))
(let ((e85 (bvslt e39 ((_ zero_extend 10) e29))))
(let ((e86 (distinct e30 ((_ sign_extend 4) e17))))
(let ((e87 (bvsge ((_ sign_extend 4) e9) e30)))
(let ((e88 (bvugt v0 ((_ sign_extend 11) e25))))
(let ((e89 (= ((_ zero_extend 11) e33) e21)))
(let ((e90 (distinct ((_ sign_extend 7) e29) e13)))
(let ((e91 (bvslt ((_ zero_extend 11) e25) e21)))
(let ((e92 (= e16 e35)))
(let ((e93 (bvsgt e23 e21)))
(let ((e94 (bvsle e11 e5)))
(let ((e95 (bvugt ((_ zero_extend 11) e35) v0)))
(let ((e96 (bvslt e22 ((_ zero_extend 6) v3))))
(let ((e97 (distinct ((_ zero_extend 11) e6) e31)))
(let ((e98 (bvugt e16 e7)))
(let ((e99 (bvsge v4 ((_ zero_extend 5) e14))))
(let ((e100 (bvsgt e8 ((_ sign_extend 7) e19))))
(let ((e101 (bvsle e31 e8)))
(let ((e102 (bvult e27 e16)))
(let ((e103 (bvslt ((_ zero_extend 8) e29) v4)))
(let ((e104 (bvslt e39 ((_ sign_extend 10) e19))))
(let ((e105 (bvslt e39 ((_ sign_extend 10) e29))))
(let ((e106 (bvsgt e32 ((_ zero_extend 10) e18))))
(let ((e107 (bvsle e21 ((_ sign_extend 11) e40))))
(let ((e108 (bvult ((_ zero_extend 4) e36) e19)))
(let ((e109 (bvsle v1 ((_ zero_extend 4) e25))))
(let ((e110 (bvugt ((_ sign_extend 5) e14) e15)))
(let ((e111 (bvsgt e32 ((_ zero_extend 14) e9))))
(let ((e112 (distinct e22 e22)))
(let ((e113 (bvugt e6 e38)))
(let ((e114 (bvule v1 ((_ zero_extend 4) e17))))
(let ((e115 (bvule v2 ((_ sign_extend 6) e16))))
(let ((e116 (bvuge e15 ((_ sign_extend 12) e40))))
(let ((e117 (= e10 e35)))
(let ((e118 (bvugt ((_ sign_extend 8) e22) e39)))
(let ((e119 (bvule ((_ sign_extend 4) e36) e19)))
(let ((e120 (bvsge ((_ sign_extend 14) e9) e37)))
(let ((e121 (= e14 ((_ sign_extend 7) e16))))
(let ((e122 (bvult ((_ sign_extend 14) e9) e32)))
(let ((e123 (bvuge e28 ((_ zero_extend 1) e23))))
(let ((e124 (ite e56 e92 e77)))
(let ((e125 (and e117 e47)))
(let ((e126 (=> e120 e82)))
(let ((e127 (or e122 e107)))
(let ((e128 (ite e108 e123 e102)))
(let ((e129 (or e91 e124)))
(let ((e130 (not e110)))
(let ((e131 (or e121 e78)))
(let ((e132 (ite e69 e104 e118)))
(let ((e133 (xor e72 e128)))
(let ((e134 (not e75)))
(let ((e135 (=> e64 e58)))
(let ((e136 (and e103 e134)))
(let ((e137 (=> e48 e60)))
(let ((e138 (and e98 e44)))
(let ((e139 (or e54 e70)))
(let ((e140 (=> e94 e74)))
(let ((e141 (=> e105 e63)))
(let ((e142 (and e133 e106)))
(let ((e143 (or e52 e115)))
(let ((e144 (=> e93 e130)))
(let ((e145 (xor e100 e86)))
(let ((e146 (= e96 e140)))
(let ((e147 (=> e142 e138)))
(let ((e148 (ite e135 e57 e55)))
(let ((e149 (or e109 e129)))
(let ((e150 (and e127 e101)))
(let ((e151 (not e84)))
(let ((e152 (= e148 e141)))
(let ((e153 (and e146 e116)))
(let ((e154 (xor e90 e49)))
(let ((e155 (and e153 e88)))
(let ((e156 (ite e99 e149 e42)))
(let ((e157 (or e65 e65)))
(let ((e158 (and e59 e80)))
(let ((e159 (ite e61 e53 e61)))
(let ((e160 (xor e156 e79)))
(let ((e161 (xor e126 e131)))
(let ((e162 (not e136)))
(let ((e163 (ite e144 e114 e160)))
(let ((e164 (xor e41 e154)))
(let ((e165 (or e62 e137)))
(let ((e166 (and e162 e46)))
(let ((e167 (and e67 e81)))
(let ((e168 (or e139 e147)))
(let ((e169 (=> e113 e163)))
(let ((e170 (= e145 e157)))
(let ((e171 (and e85 e168)))
(let ((e172 (and e119 e111)))
(let ((e173 (ite e125 e165 e83)))
(let ((e174 (and e87 e87)))
(let ((e175 (and e132 e150)))
(let ((e176 (= e170 e158)))
(let ((e177 (= e166 e45)))
(let ((e178 (=> e43 e66)))
(let ((e179 (ite e155 e171 e173)))
(let ((e180 (xor e50 e179)))
(let ((e181 (xor e174 e143)))
(let ((e182 (ite e112 e169 e89)))
(let ((e183 (and e68 e76)))
(let ((e184 (=> e180 e177)))
(let ((e185 (not e97)))
(let ((e186 (ite e176 e172 e161)))
(let ((e187 (not e159)))
(let ((e188 (or e183 e164)))
(let ((e189 (or e175 e167)))
(let ((e190 (=> e95 e189)))
(let ((e191 (or e184 e188)))
(let ((e192 (or e71 e151)))
(let ((e193 (xor e185 e51)))
(let ((e194 (and e73 e191)))
(let ((e195 (or e182 e193)))
(let ((e196 (xor e178 e192)))
(let ((e197 (and e152 e194)))
(let ((e198 (not e181)))
(let ((e199 (=> e197 e196)))
(let ((e200 (not e198)))
(let ((e201 (= e190 e195)))
(let ((e202 (not e201)))
(let ((e203 (=> e199 e187)))
(let ((e204 (= e186 e200)))
(let ((e205 (= e203 e204)))
(let ((e206 (and e202 e205)))
(let ((e207 (and e206 (not (= e12 (_ bv0 12))))))
(let ((e208 (and e207 (not (= e12 (bvnot (_ bv0 12)))))))
(let ((e209 (and e208 (not (= e37 (_ bv0 15))))))
(let ((e210 (and e209 (not (= e37 (bvnot (_ bv0 15)))))))
e210
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
